enrich
   aubifs-base
with
   

   
   
   functions  orphans : node-store × node-index → key-set;
   predicates  ubifs-cons : node-store × node-index × key-set × node-index × key-set × address-list;
               ri-cons : node-index × node-store;
               ri-inj : node-index;
               key-cons : key × node;
               log-cons : address-list × node-store;
               node-cons : key × node;
               ri-closed : node-index × node-store × key-set;
               node-closed : node × node-index × node-store × key-set;
               file-node-cons : node-store × node-index;
               . .inodes? : key-set;
   
   
   
   

   

   axioms file-node-cons
          :  ⊦ file-node-cons(fs, ri) ↔ (∀ ino. inodekey(ino) ∈ ri ∧ ¬ fs[ri[inodekey(ino)]].directory → fs[ri[inodekey(ino)]].nsubdirs = 0);
          ubifs-cons
          : ⊦   ubifs-cons(fs, ri, ro, fi, fo, log)
              ↔   ¬ inodekey(0) ∈ ri ∧ ri-cons(ri, fs) ∧ log-cons(log, fs) ∧ ¬ dups(log) ∧ ri-closed(ri, fs, ro) ∧ ro.inodes? ∧ fo.inodes?
                ∧ ro ⊆ dom ri ∧ fo ⊆ dom fi;
          orphans :  ⊦ key ∈ orphans(fs, ri) ↔ key.inode? ∧ key ∈ ri ∧ fs[ri[key]].nlink = 0 ∧ key.ino ≠ ROOT_INO;
          used for: s, ls;
          inode-set :  ⊦ ks.inodes? ↔ (∀ key. key ∈ ks → key.inode?);
          ri-inj :  ⊦ ri-inj(ri) ↔ (∀ key0, key1. key0 ∈ ri ∧ key1 ∈ ri ∧ ri[key0] = ri[key1] → key0 = key1);
          used for: ls;
          ri-cons :  ⊦ ri-cons(ri, fs) ↔ (∀ key. key ∈ ri → ri[key] ∈ fs ∧ key-cons(key, fs[ri[key]]));
          used for: ls;
          key-cons
          :  ⊦ key-cons(key, nd) ↔ nd.key = key ∧ (key.inode? → nd.inode? ∧ key.ino ≠ 0) ∧ (key.dentry? → nd.dentry?) ∧ (key.data? → nd.data?);
          log-cons :  ⊦ log-cons(log, fs) ↔ (∀ adr. adr ∈ log → adr ∈ fs ∧ node-cons(fs[adr].key, fs[adr]));
          used for: ls;
          node-cons
          : ⊦   node-cons(key, nd)
              ↔ (nd.inode? → key.inode? ∧ key.ino ≠ 0) ∧ (nd.dentry? → key.dentry?) ∧ (nd.data? → key.data?) ∧ (nd.trunc? → key.inode?);
          ri-closed :  ⊦ ri-closed(ri, fs, ro) ↔ (∀ key. key ∈ ri → ri[key] ∈ fs ∧ node-closed(fs[ri[key]], ri, fs, ro));
          used for: ls;
          node-closed
          : ⊦   node-closed(nd, ri, fs, ro)
              ↔   (  nd.dentry?
                   →   inodekey(nd.key.ino) ∈ ri ∧ ¬ inodekey(nd.key.ino) ∈ ro ∧ fs[ri[inodekey(nd.key.ino)]].directory ∧ inodekey(nd.ino) ∈ ri
                     ∧ ¬ inodekey(nd.ino) ∈ ro)
                ∧ (nd.data? → inodekey(nd.key.ino) ∈ ri ∧ ¬ fs[ri[inodekey(nd.key.ino)]].directory ∧ # nd.data = VFS_PAGE_SIZE);

   

   
end enrich